package milecToMinisat;

import java.io.File;

/**
 * Executable class performing "show and follow in terminal" test.	
 * 
* @author ter-topcased-ups
* @version 0.01, 2008/12/03
* @see 
*/
public class Test {

	private static Converter theTestConverter  = new Converter() ;
	private static String minisat ;
	
	/**
	 * perform  a "show and follow in terminal" test on the binary
	 * number generation
	 * @param args is ignored
	 */
	public static void genNbrBin (String args[]) {
//		7 sur 4 bits
		System.out.print("trad.genNbrBin(7, 4) ;\n") ;
		int id7 = theTestConverter.genIntegerConstant(7, 4) ;
		System.out.print(theTestConverter.getClauses()) ;
		System.out.print("*nbr"+id7+" contains 7 on 4 bit\n\n") ;
		
		//2 sur 8 bits
		System.out.print("trad.genNbrBin(2, 8) ;\n") ;
		int id2 = theTestConverter.genIntegerConstant(2, 8) ;
		System.out.print(theTestConverter.getClauses()) ;
		System.out.print("*nbr"+id2+" contains 2 on 8 bit\n\n") ;
		
		//5 sur 2 bits
		System.out.print("trad.genNbrBin(5,2) ;\n") ;
		int id5 = theTestConverter.genIntegerConstant(5, 2) ;
		System.out.print(theTestConverter.getClauses()) ;
		System.out.print("*nbr"+id5+" contains 5 on 2 bit (ie : 1)\n\n") ;	
	}
	
	/**
	 *  perform  a "show and follow in terminal" test on the whole package. 
	 *  @param args is ignored
	 */
	public static void main(String args[]) {
		/*TODO (facultatif) gerer les arguments pour differencier la partie du
		 * code a tester.
		 * exemple : 
		 * 	  			milecToMinisat.Test -genNbrBin
		 * 				milecToMinisat.Test -addition
		 * 				...
		 */
		if (args.length > 0) {
			ClauseGeneratorImpl.setMinisat(args[0]) ;
		} 
			 
		//desuet : Test.genNbrBin(args) ;
		//Test.scenario1() ;
		//Test.scenario2() ;
		//Test.scenario3() ;
		Test.scenario4() ;
	}

	static private void scenario1() {
		ClauseGenerator myGenerator = ClauseGeneratorImpl.getInstance() ;
		
		IntegerVariable x = myGenerator.declareInteger("x", 10) ;
		myGenerator.addIntegerConstraint(
				x, 
				IntegerConstraintType.equal, 
				new IntegerCst(8)
			) ;
		
		testGeneration() ;
	}
	
	static private void scenario2() {
		ClauseGenerator myGenerator = ClauseGeneratorImpl.getInstance() ;
		IntegerVariable x = myGenerator.declareInteger("x", 10) ;
		IntegerVariable y = myGenerator.declareInteger("y", 10) ;

		myGenerator.addIntegerConstraint(
				new IntegerOperation(x,IntegerOperator.addition, y), 
				IntegerConstraintType.equal, 
				new IntegerCst(5)
			) ;
		myGenerator.addIntegerConstraint(
				new IntegerOperation(x,IntegerOperator.subtraction, y), 
				IntegerConstraintType.greaterOrEqual, 
				new IntegerCst(2)
			) ;
		
		testGeneration() ;
	}

	static private void scenario3() {
		ClauseGenerator myGenerator = ClauseGeneratorImpl.getInstance() ;
		IntegerVariable x = myGenerator.declareInteger("x", 10) ;
		IntegerVariable y = myGenerator.declareInteger("y", 10) ;

		IntegerOperation tmp1 = new IntegerOperation(
				x,
				IntegerOperator.addition,
				x) ;
		
		IntegerOperation tmp2 = new IntegerOperation(
				tmp1,
				IntegerOperator.addition,
				y) ;
		
		myGenerator.addIntegerConstraint(
				tmp2, 
				IntegerConstraintType.equal, 
				new IntegerCst(5)
				) ;
		
		
		
		myGenerator.addIntegerConstraint(
				new IntegerOperation(
						new IntegerOperation(
								x,
								IntegerOperator.addition,
								x),
						IntegerOperator.addition,
						y), 
				IntegerConstraintType.equal, 
				new IntegerCst(5)
			) ;
		

		testGeneration() ;
	}
	
	static private void scenario4() {
		ClauseGenerator myGenerator = ClauseGeneratorImpl.getInstance() ;
		IntegerVariable x = myGenerator.declareInteger("x", 10) ;
		IntegerVariable y = myGenerator.declareInteger("y", 10) ;

		myGenerator.addIntegerConstraint(
				new IntegerOperation(x,IntegerOperator.multiplication, y), 
				IntegerConstraintType.equal, 
				new IntegerCst(6)
			) ;
		myGenerator.addIntegerConstraint(
				x,
				IntegerConstraintType.greater,
				new IntegerCst(1)
				) ;
		
		testGeneration() ;
	}
	
	/**
	 * Show clauses generated, perform execution with Minisat and show the 
	 * output of this execution
	 * @param aGenerator
	 */
	private static void testGeneration() {
		ClauseGenerator aGenerator = ClauseGeneratorImpl.getInstance() ;
		
		writeSeparator() ;
		println("Clauses generees :") ;
		writeSeparator() ;
		System.out.print(Converter.getInstance().getClauses()  ) ;
		writeSeparator() ;
		System.out.flush() ;
		
		if (ClauseGeneratorImpl.getMinisat()!= null) {
			try {
				File temporaryFile = File.createTempFile("autogenerated",".opb") ;
				
				aGenerator.writeIn(temporaryFile ) ;
				
				println("nom du fichier : `"+temporaryFile.getAbsolutePath()+"`") ;
				writeSeparator() ;
				
				println("Executing ...") ;
				String[] commande = {"/users/minfg/minfg29/TER/minisat+/minisat+_bignum_static" , temporaryFile.getAbsolutePath()} ;
				Process mySolver = Runtime.getRuntime().exec(commande) ;
				mySolver.waitFor() ;
				writeSeparator() ;
				java.io.InputStream resultStream = mySolver.getInputStream() ;
				java.io.InputStream errorStream = mySolver.getErrorStream() ;
				
				int sizeToRead = resultStream.available() ;
				byte[] result = new byte[sizeToRead] ;
				
				resultStream.read(result,0,sizeToRead) ;
				println("Resultat :") ;
				System.out.println(new String (result)) ;
				System.out.flush() ;
				
				
				sizeToRead = errorStream.available() ;
				if (sizeToRead > 0) {
					byte[] error = new byte[sizeToRead] ;
					
					errorStream.read(error,0,sizeToRead) ;
					System.err.println(new String(error)) ;
				}
			} catch (Exception ex) {
				System.err.println("pb avec l'ecriture") ;
			}
		} else {
			System.err.println("pas d'adresse renseignee pour minisat") ;
		}
	}
	
	/**
	 * print an asterisk line on the standart output
	 */
	private static void writeSeparator() {
		println("******************************************************") ;
	}
	
	/**
	 * print the string s on the standard output, adding a carriage return at the end.
	 * it's just an alias for System.out.pinrtln() 
	 * @param s, the string to be printed
	 */
	private static void println(String s) {
		System.out.println(s) ;
	}
	
}
